The field of the present invention is software verification and trust, and in particular relates to providing assurance to a host that a piece of software possesses a particular property.
The advent of distributed computing has increased the need for an efficient way to provide assurance to a host that a piece of software has a property. A piece of software is a set of instructions adapted to be executed by a processor on a host. An example of a processor is a general purpose microprocessor. Another example of a processor is an Application Specific Integrated Circuit (ASIC). Yet another example of a processor is a Digital Signal Processor (DSP).
An example of a property of a piece of software is the identity of the author of the software. Another example of a property is the identity of the compiler used to generate the piece of software. In certain applications, it is important to provide assurance to the host that a piece of software cannot alter the contents of a file stored on a disk drive of the computer on which the software is executed. This is another example of a property of a piece of software.
In a distributed computing environment, software (e.g., applets servlets, CGI bins, etc.) is obtained by a host from a provider. As used herein, a provider is a party that provides software that is adapted to be executed by a host. An example of a provider is a software manufacturer. Another example of a provider is a server on the World Wide Web connected to the Internet, where the server acts as a middleman, receiving software from a software manufacturer and sending software to hosts to be executed.
A host is a party that executes software. An example of a host is a client with a browser that is adapted to execute Java byte code, the client being adapted to be connected to the World Wide Web through the Internet. For example, a client computer (a host) with a browser obtains a Java applet from a server (a provider) on the World Wide Web over the Internet. The client executes the software, hoping that the software will not have any malicious properties, either intended or accidental, such as infecting the client with a virus, improperly altering files stored on the client, or sending private information stored on the client to another computer connected to the Internet.
Certain known systems provide the client with assurance that the software will not act improperly or maliciously, i.e., that the software has certain properties that preclude such behavior. However, these known systems are of limited usefulness, and can be expensive and inefficient to implement.
One known system for providing assurance relies upon the software provider to extensively test the software once the software is received from the software manufacturer. In one embodiment of this system, a provider tests the software under many possible conditions. If the software passes the tests, then the provider agrees to distribute the software to a host that trusts the provider.
This known system of provider testing can be disadvantageously unreliable because most software cannot be tested under all possible conditions. It is therefor possible that software that passes all of the tests could prove to be harmful when it is used under untested conditions. Further, if the nature of the tests become known by an adverse party, malicious features purposely designed to circumvent the tests could be inserted into the software. This could prove devastating to the host.
If the provider has access to the software manufacturer's source code, it can be easier for the provider to test certain properties of the software statically (without executing the software). But many software manufacturers are reluctant to release source code because it discloses valuable intellectual property (e.g., trade secrets) that is more valuable if kept confidential.
One known system for providing assurance as to the properties of source code is implemented in the Java programming language. Java byte code contains the same information as Java source code. Byte code is portable compiled code that is ready to be interpreted on a platform using a Java interpreter. Java byte code is verified every time a Java applet is received and before it is executed. Software is said to be verified when it is analyzed and determined to possess a particular property. For example, a piece of software can be verified to possess the property of not writing data to any file stored on a host. A "verifier" is a first piece of software adapted to be executed by a processor to verify a second piece of software. Known browsers, such as certain version of the Netscape Navigator manufactured by the Netscape Communications company, include Java verifiers that verify Java byte code before it is executed.
Java byte code can be verified statically. Byte code is verified statically when it is analyzed by examining the code itself, rather than analyzing its behavior when it is executed. Byte code that is verified by examining its behavior when it is executed is said to be dynamically verified.
An example of property verified in Java byte code by a Java byte code verifier is that a piece of Java byte code contains no type errors. A static type-inference analysis is carried to ensure, for example, that a variable A of type char (character) is not used in the code in such a way as to produce a type error (e.g., type char variable A is not used in arithmetic expressions with floating point variables to yield an integer, i.e., a character string is not added to a real number to yield an integer). If the Java code is approved by the verifier, then it provides a reasonable (as yet formally unproven) basis for the host to conclude the byte code possesses the property of not giving rise to type errors during execution.
However, the verifier can be imperfect, and can indicate that a piece of Java byte code has a property when in fact it does not, at least under certain conditions. Also, analyzing Java byte code every time before it is executed to determine if it has a property disadvantageously imposes a significant burden on the host, especially for analyzing the byte code of large applets.
Because it is imperfect, the Java verifier is continually under development. As used herein, a "verifier" is a set of verification instructions adapted to be executed by a processor to determine if a piece of software (called a "set of subject instructions", or "subject set") possesses a particular property. When a flaw is found in the verifier, the verifier must be revised and updated. Distributing the latest version of the Java verifier is logistically difficult, because the verifier resides at every local platform that executes Java code. For example, the verifier resides in millions of copies of the Netscape browser manufactured by the Netscape Communications company, and it is unlikely that every such browser executes the latest updated version of the Java verifier. Thus, outdated verifiers are widely used, providing a diminished level of security by operating with weaknesses that can be widely known and exploited.
Another approach to providing assurance is provided by formal verification. Software that is formally verified is analyzed mathematically to prove that the software has a property. Formal verification is generally carried out by the host because the provider remains untrusted. Even if the host provides trusted formal verification software to the provider, there is no guarantee that the formal verification software will not be compromised in some way at the provider's site, and thus improperly analyze harmful software without detecting its harmful aspects. Formal verification techniques are also unwieldy, and can often be impractical to implement for software of any real complexity.
The problem of dealing with an untrusted provider has been addressed in one known system by having the provider construct a proof of establishing that a piece of software has a property, and shipping the proof along with the binary version of the software to the host. The binary program is annotated to enable the construction of a verification condition by the host. If the host can establish the verification condition, then the host is assured that the software has the property. This advantageously reduces the burden on the host, which must only check the proof, which can be carried out much more quickly and easily than having to construct the proof.
Although generally faster than proof construction, proof checking can still prove to be a substantial task, depending upon the size of the proof. In the case of highly mobile code, such as applets and agents, the proof must be checked for each execution, which can incur unacceptably high overhead for the host. Also, proof checkers are installed and executed on the host computer, and are thus subject to the same logistical problems (distribution and maintenance of updates) as for the Java verifier. Also, in order for proof checking to be effective, the full proof and any invariants that contribute to the proof have to be released by the provider to the host. The disclosure of invariants can actually reveal more valuable proprietary information than the disclosure of source code. Such a disclosure of invariants can disadvantageously compromise the confidentiality and therefore the value of certain of the software manufacturer's intellectual property.
Another method of providing assurance in an automated fashion is the ActiveX model. ActiveX is based upon the assumption that software built by well-known individuals or companies can be trusted. The authenticity of the software is established by an attached cryptographic signature. If the key of the signature corresponds to a key in a trusted group, then the software is accepted and executed without requiring any further static or dynamic checks. Signature checking is very quick, and adds little overhead.
However, the trust provided by the ActiveX system is based only upon establishing the identity of the manufacturer and not more. Relying entirely on the reputation of a manufacturer can be risky. Further, if the cryptographic keys are stolen or misused, signed (and hence trusted) software could wreak havoc on a host. Likewise, if a trusted insider with a trusted key builds malicious software and signs it, the malicious software will be accepted and run without further checking, possibly with disastrous results.
Under yet another known system, providers can have their software tested by a third party that is trusted by the host. The third party analyzes and then signs software if the analysis shows the software to possess a property. The process of analyzing and then signing a piece of software if the analysis shows the software to possess a property is termed "certification". However, the provider must trust the third party to maintain the confidentiality of the testing process and of any intellectual property belonging to the manufacturer. This can make a manufacturer reluctant to use this known system.
In summary, analyzing software properties locally (at the host) can be impractical (particularly in distributed systems) because an updated verifier has to be universally distributed every time a security weakness and/or flaw is discovered in the present version of the verifier. Formally verifying source code at the host can be impractical, burdensome, and involve the disclosure of intellectual property that the software manufacturer would prefer to keep confidential. Having a third party analyze the software and sign it reduces the burden placed on the host and can involve fewer logistical problems, but fails if the third party breaches its trust, or if cryptographic keys are mismanaged.